\begin{tabbing}
$\forall$\=$i$, $x$:Id, $k$:Knd, ${\it ds}$:$a$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type,\+
\\[0ex]$f$:(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$${\it ds}$($x$)?Void).
\-\\[0ex]@$i$: with declarations ds:${\it ds}$da:${\it da}$effect of $k$(v) is $x$ := $f$ s v $\in$ Dsys
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@$i$: with declarations ds:${\it ds}$da:${\it da}$effect of $k$(v) is $x$ := $f$ s v $\subseteq$ $D$
\\[0ex]$\Rightarrow$ \=$D$ \+
\\[0ex]realizes ${\it es}$.
\\[0ex]($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]\& ($\forall$$e$:E. loc($e$) $=$ $i$ $\in$ Id $\Rightarrow$ valtype($e$) $\subseteq\rho$ Valtype(${\it da}$;kind($e$)))
\\[0ex]\& ((isrcv($k$) $\Rightarrow$ destination(lnk($k$)) $=$ $i$) $\Rightarrow$ kindtype($i$;$k$) $\subseteq\rho$ Valtype(${\it da}$;$k$))
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]loc($e$) $=$ $i$ $\in$ Id
\\[0ex]$\Rightarrow$ kind($e$) $=$ $k$ $\in$ Knd
\\[0ex]$\Rightarrow$ ($x$ after $e$) $=$ $f$((state when $e$),val($e$)) $\in$ ${\it ds}$($x$)?Top))
\-\-\-
\end{tabbing}